perm filename CONTEX[W90,JMC] blob sn#883176 filedate 1990-03-20 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	%contex[w90,jmc]		Notes for paper on context
C00006 ENDMK
C⊗;
%contex[w90,jmc]		Notes for paper on context

1. relations among contexts
	conceptual specialization, formal dropping of arguments

2. entering a person's knowledge or belief.  Then one can
reason using ordinary logic and then revert.  Does this do
all we want?  Can we avoid any other rules for knowledge of
quantified expressions?  What rules for knowledge of
quantified expressions would it give us?  In ordinary modal
logic, can we enter the world (context) of necessity or a possible world.
What if the person whose belief is being entered is variable?
Entering a possible world would require saying which possible
world somehow, because otherwise you get in trouble with
incompatible possible propositions.  We could assume one
possible proposition.  This is like natural deduction restricted
to assuming possible propositions.  What does such a restriction
get us?

If we enter knowledge outer propositions are preserved.  Entering
beliefs requires defaults assumptions about what truths are believed.
When we enter someone's knowledge or belief, we will still have
to import the beliefs one at a time.

3. Non-knowledge is used as follows:

	Suppose we have ¬K(John,p) and want to prove ¬K(John,q).  We say
assume K(John,q)
enter knowledge John
this gives
	q

we then infer by some reasoning process
	p
We can then write, leaving John's knowledge
K(John,p)
which contradicts ¬K(John,p)
which allows inferring the negation of the assumption K(John,q) getting
¬K(John,q).

Can these tricks do the Wise Men puzzle or Mr. S and Mr. P?

Yes, it does the Wise Man Puzzle nicely in the simple form.
What about using it to prove non-knowledge starting from
``All he knows is π''
Here's how it goes.  
Give a consistent set of propositions and show that it implies π.
How do we know a set of propositions is consistent?  A set of
distinct literals is consistent.  What else?  What in the predicate
calculus?  What about proving that a model is consistent with
Peano arithmetic, i.e. with induction?  Looks like we need the consistency axiom.